(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
pairNs → cons(0, n__incr(n__oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__oddNs) → oddNs
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__repItems(X)) → repItems(activate(X))
activate(X) → X
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
activate(n__incr(X)) →+ incr(activate(X))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [X / n__incr(X)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
pairNs → cons(0', n__incr(n__oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0', XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__oddNs) → oddNs
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__repItems(X)) → repItems(activate(X))
activate(X) → X
S is empty.
Rewrite Strategy: INNERMOST
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
Innermost TRS:
Rules:
pairNs → cons(0', n__incr(n__oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0', XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__oddNs) → oddNs
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__repItems(X)) → repItems(activate(X))
activate(X) → X
Types:
pairNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
0' :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
s :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
activate :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
nil :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
pair :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
tail :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
hole_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons1_0 :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0 :: Nat → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
oddNs,
incr,
activate,
repItemsThey will be analysed ascendingly in the following order:
oddNs = incr
oddNs = activate
oddNs = repItems
incr = activate
incr = repItems
activate = repItems
(8) Obligation:
Innermost TRS:
Rules:
pairNs →
cons(
0',
n__incr(
n__oddNs))
oddNs →
incr(
pairNs)
incr(
cons(
X,
XS)) →
cons(
s(
X),
n__incr(
activate(
XS)))
take(
0',
XS) →
niltake(
s(
N),
cons(
X,
XS)) →
cons(
X,
n__take(
N,
activate(
XS)))
zip(
nil,
XS) →
nilzip(
X,
nil) →
nilzip(
cons(
X,
XS),
cons(
Y,
YS)) →
cons(
pair(
X,
Y),
n__zip(
activate(
XS),
activate(
YS)))
tail(
cons(
X,
XS)) →
activate(
XS)
repItems(
nil) →
nilrepItems(
cons(
X,
XS)) →
cons(
X,
n__cons(
X,
n__repItems(
activate(
XS))))
incr(
X) →
n__incr(
X)
oddNs →
n__oddNstake(
X1,
X2) →
n__take(
X1,
X2)
zip(
X1,
X2) →
n__zip(
X1,
X2)
cons(
X1,
X2) →
n__cons(
X1,
X2)
repItems(
X) →
n__repItems(
X)
activate(
n__incr(
X)) →
incr(
activate(
X))
activate(
n__oddNs) →
oddNsactivate(
n__take(
X1,
X2)) →
take(
activate(
X1),
activate(
X2))
activate(
n__zip(
X1,
X2)) →
zip(
activate(
X1),
activate(
X2))
activate(
n__cons(
X1,
X2)) →
cons(
activate(
X1),
X2)
activate(
n__repItems(
X)) →
repItems(
activate(
X))
activate(
X) →
XTypes:
pairNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
0' :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
s :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
activate :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
nil :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
pair :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
tail :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
hole_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons1_0 :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0 :: Nat → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
Generator Equations:
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(0) ⇔ 0'
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(x, 1)) ⇔ n__incr(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(x))
The following defined symbols remain to be analysed:
incr, oddNs, activate, repItems
They will be analysed ascendingly in the following order:
oddNs = incr
oddNs = activate
oddNs = repItems
incr = activate
incr = repItems
activate = repItems
(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol incr.
(10) Obligation:
Innermost TRS:
Rules:
pairNs →
cons(
0',
n__incr(
n__oddNs))
oddNs →
incr(
pairNs)
incr(
cons(
X,
XS)) →
cons(
s(
X),
n__incr(
activate(
XS)))
take(
0',
XS) →
niltake(
s(
N),
cons(
X,
XS)) →
cons(
X,
n__take(
N,
activate(
XS)))
zip(
nil,
XS) →
nilzip(
X,
nil) →
nilzip(
cons(
X,
XS),
cons(
Y,
YS)) →
cons(
pair(
X,
Y),
n__zip(
activate(
XS),
activate(
YS)))
tail(
cons(
X,
XS)) →
activate(
XS)
repItems(
nil) →
nilrepItems(
cons(
X,
XS)) →
cons(
X,
n__cons(
X,
n__repItems(
activate(
XS))))
incr(
X) →
n__incr(
X)
oddNs →
n__oddNstake(
X1,
X2) →
n__take(
X1,
X2)
zip(
X1,
X2) →
n__zip(
X1,
X2)
cons(
X1,
X2) →
n__cons(
X1,
X2)
repItems(
X) →
n__repItems(
X)
activate(
n__incr(
X)) →
incr(
activate(
X))
activate(
n__oddNs) →
oddNsactivate(
n__take(
X1,
X2)) →
take(
activate(
X1),
activate(
X2))
activate(
n__zip(
X1,
X2)) →
zip(
activate(
X1),
activate(
X2))
activate(
n__cons(
X1,
X2)) →
cons(
activate(
X1),
X2)
activate(
n__repItems(
X)) →
repItems(
activate(
X))
activate(
X) →
XTypes:
pairNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
0' :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
s :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
activate :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
nil :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
pair :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
tail :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
hole_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons1_0 :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0 :: Nat → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
Generator Equations:
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(0) ⇔ 0'
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(x, 1)) ⇔ n__incr(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(x))
The following defined symbols remain to be analysed:
activate, oddNs, repItems
They will be analysed ascendingly in the following order:
oddNs = incr
oddNs = activate
oddNs = repItems
incr = activate
incr = repItems
activate = repItems
(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol activate.
(12) Obligation:
Innermost TRS:
Rules:
pairNs →
cons(
0',
n__incr(
n__oddNs))
oddNs →
incr(
pairNs)
incr(
cons(
X,
XS)) →
cons(
s(
X),
n__incr(
activate(
XS)))
take(
0',
XS) →
niltake(
s(
N),
cons(
X,
XS)) →
cons(
X,
n__take(
N,
activate(
XS)))
zip(
nil,
XS) →
nilzip(
X,
nil) →
nilzip(
cons(
X,
XS),
cons(
Y,
YS)) →
cons(
pair(
X,
Y),
n__zip(
activate(
XS),
activate(
YS)))
tail(
cons(
X,
XS)) →
activate(
XS)
repItems(
nil) →
nilrepItems(
cons(
X,
XS)) →
cons(
X,
n__cons(
X,
n__repItems(
activate(
XS))))
incr(
X) →
n__incr(
X)
oddNs →
n__oddNstake(
X1,
X2) →
n__take(
X1,
X2)
zip(
X1,
X2) →
n__zip(
X1,
X2)
cons(
X1,
X2) →
n__cons(
X1,
X2)
repItems(
X) →
n__repItems(
X)
activate(
n__incr(
X)) →
incr(
activate(
X))
activate(
n__oddNs) →
oddNsactivate(
n__take(
X1,
X2)) →
take(
activate(
X1),
activate(
X2))
activate(
n__zip(
X1,
X2)) →
zip(
activate(
X1),
activate(
X2))
activate(
n__cons(
X1,
X2)) →
cons(
activate(
X1),
X2)
activate(
n__repItems(
X)) →
repItems(
activate(
X))
activate(
X) →
XTypes:
pairNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
0' :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
s :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
activate :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
nil :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
pair :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
tail :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
hole_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons1_0 :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0 :: Nat → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
Generator Equations:
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(0) ⇔ 0'
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(x, 1)) ⇔ n__incr(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(x))
The following defined symbols remain to be analysed:
oddNs, repItems
They will be analysed ascendingly in the following order:
oddNs = incr
oddNs = activate
oddNs = repItems
incr = activate
incr = repItems
activate = repItems
(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol oddNs.
(14) Obligation:
Innermost TRS:
Rules:
pairNs →
cons(
0',
n__incr(
n__oddNs))
oddNs →
incr(
pairNs)
incr(
cons(
X,
XS)) →
cons(
s(
X),
n__incr(
activate(
XS)))
take(
0',
XS) →
niltake(
s(
N),
cons(
X,
XS)) →
cons(
X,
n__take(
N,
activate(
XS)))
zip(
nil,
XS) →
nilzip(
X,
nil) →
nilzip(
cons(
X,
XS),
cons(
Y,
YS)) →
cons(
pair(
X,
Y),
n__zip(
activate(
XS),
activate(
YS)))
tail(
cons(
X,
XS)) →
activate(
XS)
repItems(
nil) →
nilrepItems(
cons(
X,
XS)) →
cons(
X,
n__cons(
X,
n__repItems(
activate(
XS))))
incr(
X) →
n__incr(
X)
oddNs →
n__oddNstake(
X1,
X2) →
n__take(
X1,
X2)
zip(
X1,
X2) →
n__zip(
X1,
X2)
cons(
X1,
X2) →
n__cons(
X1,
X2)
repItems(
X) →
n__repItems(
X)
activate(
n__incr(
X)) →
incr(
activate(
X))
activate(
n__oddNs) →
oddNsactivate(
n__take(
X1,
X2)) →
take(
activate(
X1),
activate(
X2))
activate(
n__zip(
X1,
X2)) →
zip(
activate(
X1),
activate(
X2))
activate(
n__cons(
X1,
X2)) →
cons(
activate(
X1),
X2)
activate(
n__repItems(
X)) →
repItems(
activate(
X))
activate(
X) →
XTypes:
pairNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
0' :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
s :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
activate :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
nil :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
pair :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
tail :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
hole_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons1_0 :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0 :: Nat → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
Generator Equations:
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(0) ⇔ 0'
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(x, 1)) ⇔ n__incr(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(x))
The following defined symbols remain to be analysed:
repItems
They will be analysed ascendingly in the following order:
oddNs = incr
oddNs = activate
oddNs = repItems
incr = activate
incr = repItems
activate = repItems
(15) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol repItems.
(16) Obligation:
Innermost TRS:
Rules:
pairNs →
cons(
0',
n__incr(
n__oddNs))
oddNs →
incr(
pairNs)
incr(
cons(
X,
XS)) →
cons(
s(
X),
n__incr(
activate(
XS)))
take(
0',
XS) →
niltake(
s(
N),
cons(
X,
XS)) →
cons(
X,
n__take(
N,
activate(
XS)))
zip(
nil,
XS) →
nilzip(
X,
nil) →
nilzip(
cons(
X,
XS),
cons(
Y,
YS)) →
cons(
pair(
X,
Y),
n__zip(
activate(
XS),
activate(
YS)))
tail(
cons(
X,
XS)) →
activate(
XS)
repItems(
nil) →
nilrepItems(
cons(
X,
XS)) →
cons(
X,
n__cons(
X,
n__repItems(
activate(
XS))))
incr(
X) →
n__incr(
X)
oddNs →
n__oddNstake(
X1,
X2) →
n__take(
X1,
X2)
zip(
X1,
X2) →
n__zip(
X1,
X2)
cons(
X1,
X2) →
n__cons(
X1,
X2)
repItems(
X) →
n__repItems(
X)
activate(
n__incr(
X)) →
incr(
activate(
X))
activate(
n__oddNs) →
oddNsactivate(
n__take(
X1,
X2)) →
take(
activate(
X1),
activate(
X2))
activate(
n__zip(
X1,
X2)) →
zip(
activate(
X1),
activate(
X2))
activate(
n__cons(
X1,
X2)) →
cons(
activate(
X1),
X2)
activate(
n__repItems(
X)) →
repItems(
activate(
X))
activate(
X) →
XTypes:
pairNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
0' :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
s :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
activate :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
nil :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
pair :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
tail :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
hole_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons1_0 :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0 :: Nat → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
Generator Equations:
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(0) ⇔ 0'
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(x, 1)) ⇔ n__incr(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(x))
No more defined symbols left to analyse.